w:World, e:E. ((first(e)))  (time(pred(e)) < time(e)) 

latex

Definitions	b, isl(x), w-pred(w;e), a < b, time(e), x.A(x), World, first(e), P  Q, P & Q, x:A  B(x), x:AB(x), b, Dec(P), P  Q, left + right, E, Type, Unit, x:A. B(x), t  T, A, P  Q, False, <a, b>, n - m, #$n, i  j , pred(e), (i = j), ff, isnull(a), a(i;t), , , outl(x), Void, A  B, s = t, , n+m, -n, True, t.2, x. t(x), {x:A| B(x)} , Id,
Lemmas	nat wf, Id wf, pi2 wf, false wf, true wf, le wf, w-pred-wf2, bool wf, w-a wf, w-isnull wf, eqff to assert, iff transitivity, eqtt to assert, eq int wf, assert of eq int, nat properties, ge wf, w-pred wf, unit wf, w-E wf, isl wf, decidable assert, assert wf, not wf, bnot wf, assert of bnot, not functionality wrt iff, world wf, first wf